A:Type, f:(A), L:A List. b2of(split_tail(L | x.f(x))). f(b) 

latex

Definitions	b, t  T, x:A. B(x), , x(s), Prop, x. t(x), xL. P(x), P  Q, A, b, P & Q, P  Q, Unit, split_tail(L | x.f(x)), P  Q
Lemmas	l all cons, split tail wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, l all wf, l all nil, assert wf, bool wf